PL wiki

마틴뢰프 타입 이론

  • 타입 이론

마틴뢰프 타입 이론(Martin-Löf type theory, MLTT)은 페르 마틴뢰프가 고안한 타입 이론의 한가지이다.

판단

MLTT에는 4가지 종류의 기본적인 판단이 있다. \[ \begin{array}{l} A \ \mathrm{type} \\ A \equiv B \ \mathrm{type} \\ M : A \\ M \equiv N : A \end{array} \] 이들은 각각 다음을 의미한다.

현대적인 형식화에서는 주로 맥락 \(\Gamma\)가 추가된 형태의 판단을 사용한다. \[ \newcommand{\type}[2] {#1 \vdash #2 \ \mathrm{type}} \newcommand{\typeeq}[3] {#1 \vdash #2 \equiv #3 \ \mathrm{type}} \newcommand{\term}[3] {#1 \vdash #2 : #3} \newcommand{\termeq}[4] {#1 \vdash #2 \equiv #3 : #4} \begin{array}{l} \type{\Gamma}{A} \\ \typeeq{\Gamma}{A}{B} \\ \term{\Gamma}{M}{A} \\ \termeq{\Gamma}{M}{N}{A} \end{array} \]

타입 형성자

각각의 타입 형성자들은 형성 규칙(formation rule), 도입 규칙(introduction rule), 소거 규칙(elimination rule), 계산 규칙(computation rule), 유일성 규칙(uniqueness rule)을 가진다.

\(\Pi\)-타입

\[ \begin{prooftree} \AXC{ $\type{\Gamma}{A}$ } \AXC{ $\type{\Gamma, x:A}{B}$ } \RL{ $\Pi\text{-FORM}$ } \BIC{ $\type{\Gamma}{\prod_{x:A} B}$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\term{\Gamma, x:A}{b}{B}$ } \RL{ $\Pi\text{-INTRO}$ } \UIC{ $\term{\Gamma}{\lambda x . b}{\prod_{x:A} B}$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\term{\Gamma}{f}{\prod_{x:A} B}$ } \AXC{ $\term{\Gamma}{a}{A}$ } \RL{ $\Pi\text{-ELIM}$ } \BIC{ $\term{\Gamma}{f \ a}{B[a/x]}$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\term{\Gamma, x:A}{b}{B}$ } \AXC{ $\term{\Gamma}{a}{A}$ } \RL{ $\Pi\text{-COMP}$ } \BIC{ $\termeq{\Gamma}{(\lambda x. b) \ a}{b[a/x]}{B[a/x]}$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\term{\Gamma}{f}{\prod_{x:A} B}$ } \RL{ $\Pi\text{-UNIQ}$ } \UIC{ $\termeq{\Gamma}{f}{(\lambda x. f \ x)}{\prod_{x:A} B}$ } \end{prooftree} \]

\(\Sigma\)-타입

\(\Sigma\)-타입은 양성적/음성적 두가지 방법으로 정의할 수 있다. \[ \begin{prooftree} \AXC{ $\type{\Gamma}{A}$ } \AXC{ $\type{\Gamma,x:A}{B}$ } \RL{ $\Sigma\text{-FORM}$ } \BIC{ $\type{\Gamma}{\sum_{x:A} B}$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\term{\Gamma}{a}{A}$ } \AXC{ $\term{\Gamma}{b}{B[a/x]}$ } \RL{ $\Sigma\text{-INTRO}$ } \BIC{ $\term{\Gamma}{ \langle a,b \rangle }{\sum_{x:A} B}$ } \end{prooftree} \]

양성적 정의

\[ \newcommand{\ind}[0] {\mathbf{ind}} \begin{prooftree} \AXC{ $\type{\Gamma,z:\sum_{x:A}B}{C}$ } \AXC{ $\term{\Gamma,x:A,y:B}{c}{C[\langle x,y \rangle / z]}$ } \AXC{ $\term{\Gamma}{p}{\sum_{x:A} B}$ } \RL{ $\Sigma\text{-ELIM}^+$ } \TrinaryInfC{ $\term{\Gamma}{\ind_{\sum_{x:A} B}(z.C, x.y.c, p)}{C[p/z]}$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\type{\Gamma,z:\sum_{x:A}B}{C}$ } \AXC{ $\term{\Gamma,x:A,y:B}{c}{C[\langle x,y \rangle / z]}$ } \AXC{ $\term{\Gamma}{a}{A}$ } \AXC{ $\term{\Gamma}{b}{B[a/x]}$ } \RL{ $\Sigma\text{-COMP}^+$ } \QuaternaryInfC{ $\termeq{\Gamma}{\ind_{\sum_{x:A} B}(z.C, x.y.c, \langle a, b \rangle)}{c[a/x,b/y]}{C[\langle a, b \rangle / z]}$ } \end{prooftree} \]

음성적 정의

\[ \newcommand{\fst}[0] {\mathbf{fst}} \newcommand{\snd}[0] {\mathbf{snd}} \begin{prooftree} \AXC{ $\term{\Gamma}{p}{\sum_{x:A} B}$ } \RL{ $\Sigma\text{-ELIM}_1^-$ } \UIC{ $\term{\Gamma}{\fst(p)}{A}$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\term{\Gamma}{p}{\sum_{x:A} B}$ } \RL{ $\Sigma\text{-ELIM}_2^-$ } \UIC{ $\term{\Gamma}{\snd(p)}{B[\fst(p)/x]}$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\term{\Gamma}{a}{A}$ } \AXC{ $\term{\Gamma}{b}{B[a/x]}$ } \RL{ $\Sigma\text{-COMP}^-_1$ } \BIC{ $\termeq{\Gamma}{\fst(\langle a, b \rangle)}{a}{A}$ } \end{prooftree} \quad \begin{prooftree} \AXC{ $\term{\Gamma}{a}{A}$ } \AXC{ $\term{\Gamma}{b}{B[a/x]}$ } \RL{ $\Sigma\text{-COMP}^-_2$ } \BIC{ $\termeq{\Gamma}{\snd(\langle a, b \rangle)}{b}{B[a/x]}$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\term{\Gamma}{p}{\sum_{x:A} B}$ } \RL{ $\Sigma\text{-UNIQ}^-$ } \UIC{ $\termeq{\Gamma}{p}{\langle \fst(p), \snd(p) \rangle}{\sum_{x:A} B}$ } \end{prooftree} \]

동일성 타입

\[ \begin{prooftree} \AXC{ $\type{\Gamma}{A}$ } \AXC{ $\term{\Gamma}{a}{A}$ } \AXC{ $\term{\Gamma}{b}{A}$ } \RL{ ${=}\text{-FORM}$ } \TIC{ $\type{\Gamma}{a =_A b}$ } \end{prooftree} \] \[ \newcommand{\refl}[0] {\mathbf{refl}} \begin{prooftree} \AXC{ $\term{\Gamma}{a}{A}$ } \RL{ ${=}\text{-INTRO}$ } \UIC{ $\term{\Gamma}{\refl_a}{a =_A a}$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\type{\Gamma,x:A,y:A,p:x =_A y}{C}$ } \AXC{ $\term{\Gamma,z:A}{c}{C[z/x,z/y,\refl_z/p]}$ } \AXC{ $\term{\Gamma}{a}{A}$ } \AXC{ $\term{\Gamma}{b}{A}$ } \AXC{ $\term{\Gamma}{p'}{a =_A b}$ } \RL{ ${=}\text{-ELIM}$ } \QuinaryInfC{ $\term{\Gamma}{\ind_{=_A}(x.y.p.C, z.c, a, b, p')}{C[a/x,b/y,p'/p]}$ } \end{prooftree} \] \[ \begin{prooftree} \AXC{ $\type{\Gamma,x:A,y:A,p:x =_A y}{C}$ } \AXC{ $\term{\Gamma,z:A}{c}{C[z/x,z/y,\refl_z/p]}$ } \AXC{ $\term{\Gamma}{a}{A}$ } \RL{ ${=}\text{-COMP}$ } \TIC{ $\termeq{\Gamma}{\ind_{=_A}(x.y.p.C, z.c, a, a, \refl_a)}{c[a/z]}{C[a/x,a/y,\refl_a/p]}$ } \end{prooftree} \]

\(\mathcal{W}\)-타입

\[ \begin{prooftree} \AXC{ $\type{\Gamma}{A}$ } \AXC{ $\type{\Gamma,x:A}{B}$ } \RL{ $\mathcal{W}\text{-FORM}$ } \BIC{ $\type{\Gamma}{\mathcal{W}_{x:A} B}$ } \end{prooftree} \] \[ \begin{prooftree} \newcommand{\sup}[0] {\mathbf{sup}} \AXC{ $\term{\Gamma}{a}{A}$ } \AXC{ $\term{\Gamma}{f}{B[a/x] \to \mathcal{W}_{x:A} B}$ } \RL{ $\mathcal{W}\text{-INTRO}$ } \BIC{ $\term{\Gamma}{\sup(a,f)}{\mathcal{W}_{x:A} B}$ } \end{prooftree} \] \[ \begin{prooftree} \newcommand{\sup}[0] {\mathbf{sup}} \AXC{ $\type{\Gamma,w:\mathcal{W}_{x:A} B}{C}$ } \AXC{ $\term{\Gamma,x:A,u:B \to \mathcal{W}_{x:A} B,v:\prod_{y:B} C[u \ y/w]}{c}{C[\sup(x,u)/w]}$ } \AXC{ $\term{\Gamma}{w'}{\mathcal{W}_{x:A} B}$ } \RL{ $\mathcal{W}\text{-ELIM}$ } \TIC{ $\term{\Gamma}{\ind_{\mathcal{W}_{x:A} B}(w.C, x.u.v.c, w')}{C[w'/w]}$ } \end{prooftree} \] \[ \begin{prooftree} \newcommand{\sup}[0] {\mathbf{sup}} \AXC{ $\type{\Gamma,w:\mathcal{W}_{x:A} B}{C}$ } \AXC{ $\term{\Gamma,x:A,u:B \to \mathcal{W}_{x:A} B,v:\prod_{y:B} C[u \ y/w]}{c}{C[\sup(x,u)/w]}$ } \AXC{ $\term{\Gamma}{a}{A}$ } \AXC{ $\term{\Gamma}{f}{B[a/x] \to \mathcal{W}_{x:A} B}$ } \RL{ $\mathcal{W}\text{-COMP}$ } \QuaternaryInfC{ $\termeq{\Gamma}{\ind_{\mathcal{W}_{x:A} B}(w.C, x.u.v.c, \sup(a,f))}{c[a/x,f/u,\lambda y. \ind_{\mathcal{W}_{x:A} B}(w.C,x.u.v.c,f \ y)/v]}{C[\sup(a,f)/w]}$ } \end{prooftree} \]

동일성

마틴뢰프 타입 이론에는 두 가지의 동일성 개념이 있다. 판단적 같음(judgemental equality) \(\typeeq{\Gamma}{A}{B}\)와 \(\termeq{\Gamma}{M}{N}{A}\)는 두 타입 혹은 항이 같음을 의미하는 메타 레벨에서의 서술이다. 반면에 동일성 타입(equality type, identity type, propositional equality, typal equality) \(a =_A b\)는 타입 이론 내의 두 대상이 같음을 서술하는 타입이다.